$\forall$${\it es}$:ES, $i$:Id, ${\it e'}$:E, $P$:(\{$e$:E$\mid$ loc($e$) = $i$\} $\rightarrow\mathbb{P}$).
\\[0ex]$\forall$$e$@$i$. Dec($P$($e$)) $\Rightarrow$ (loc(${\it e'}$) = $i$) $\Rightarrow$ ($\exists$$e$$<$${\it e'}$.$e$ is first@ $i$ s.t.  $e$.$P$($e$) $\Leftarrow\!\Rightarrow$ $\exists$$e$$<$${\it e'}$.$P$($e$))